package fsmCore;

import java.io.Serializable;

public abstract class Transizione implements Serializable{

	//@ invariant durata > 0

	private static final long serialVersionUID = 1L;
	// nome transizione
	private String nome;
	// stato sorgente transizione
	private Stato sorgente;
	// stato destinazione transizione
	private Stato destinazione;
	// durata transizione
	private int durata;
	// durata residua prima della fine di transizione valore default=durata
	private int durataresidua;
	
	//@ requires non_null sorgente && non_null destinazione && non_null nome
	public Transizione(Stato sorgente, Stato destinazione, String nome){
		// valgono per tutte le classi figlie
		this.sorgente=sorgente;
		this.destinazione=destinazione;
		this.nome=nome;
	}
	

	/*@ requires non_null durata  &&
	  @ requires durataresidua >= 0
	  @*/
	// metodo che ritorna true se la transizione � in atto
	public boolean isInAtto(){
		if(durata==durataresidua)
			return false;
		else
			return true;
	}

	// ritorna true se � sincrona
	abstract public boolean sincrona();
	
	public Stato getSorgente() {
		return sorgente;
	}

	//@requires non_null sorgente
	public void setSorgente(Stato sorgente) {
		this.sorgente = sorgente;
	}

	public Stato getDestinazione() {
		return destinazione;
	}

	//@ requires non_null destinazione
	public void setDestinazione(Stato destinazione) {
		this.destinazione = destinazione;
	}

	public int getDurata() {
		return durata;
	}

	//@ requires non_null durata
	public void setDurata(int durata) {
		this.durata = durata;
	}

	public int getDurataresidua() {
		return durataresidua;
	}

	//@ requires non_null durataresidua
	public void setDurataresidua(int durataresidua) {
		this.durataresidua = durataresidua;
	}

	public String getNome() {
		return nome;
	}

	//@ requires non_null nome
	public void setNome(String nome) {
		this.nome = nome;
	}
	
	abstract public String toStringDet();
	
}
